(declare-sort sort0 0)

(declare-fun x () list)
(declare-fun y () list)
(declare-fun append (list list) list)
(declare-fun bool0 () Bool)
(declare-fun bool1 () Bool)
(declare-fun bool2 () Bool)
(assert (not (= (= (append x y) y) (= x nil))))
(assert (=> true bool0))
(assert (=> (and bool0 (not (= x nil))) bool1))
(assert (let ((a!1 (ite (= x nil) y (cons (head x) (append (tail x) y))))) (= (append x y) a!1)))
(assert (let ((a!1 (and bool1 (not (= (tail x) nil))))) (=> a!1 bool2)))
(assert (let ((a!1 (cons (head (tail x)) (append (tail (tail x)) y)))) (= (append (tail x) y) (ite (= (tail x) nil) y a!1))))
(check-sat)
